Characterising Strongly Normalising Intuitionistic Sequent Terms
Identifieur interne : 004414 ( Main/Exploration ); précédent : 004413; suivant : 004415Characterising Strongly Normalising Intuitionistic Sequent Terms
Auteurs : J. Espírito Santo [Portugal] ; S. Ghilezan [Serbie] ; J. Iveti [Serbie]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: This paper gives a characterisation, via intersection types, of the strongly normalising terms of an intuitionistic sequent calculus (where LJ easily embeds). The soundness of the typing system is reduced to that of a well known typing system with intersection types for the ordinary λ-calculus. The completeness of the typing system is obtained from subject expansion at root position. This paper’s sequent term calculus integrates smoothly the λ-terms with generalised application or explicit substitution. Strong normalisability of these terms as sequent terms characterises their typeability in certain “natural” typing systems with intersection types. The latter are in the natural deduction format, like systems previously studied by Matthes and Lengrand et al., except that they do not contain any extra, exceptional rules for typing generalised applications or substitution.
Url:
DOI: 10.1007/978-3-540-68103-8_6
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 000653
- to stream Istex, to step Curation: 000648
- to stream Istex, to step Checkpoint: 000E42
- to stream Main, to step Merge: 004525
- to stream Main, to step Curation: 004414
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Characterising Strongly Normalising Intuitionistic Sequent Terms</title><author><name sortKey="Espirito Santo, J" sort="Espirito Santo, J" uniqKey="Espirito Santo J" first="J." last="Espírito Santo">J. Espírito Santo</name></author><author><name sortKey="Ghilezan, S" sort="Ghilezan, S" uniqKey="Ghilezan S" first="S." last="Ghilezan">S. Ghilezan</name></author><author><name sortKey="Iveti, J" sort="Iveti, J" uniqKey="Iveti J" first="J." last="Iveti">J. Iveti</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:1CB16E50D217A5407B98673DF326F8AF7574915B</idno><date when="2008" year="2008">2008</date><idno type="doi">10.1007/978-3-540-68103-8_6</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-N6KS52T8-N/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">000653</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">000653</idno><idno type="wicri:Area/Istex/Curation">000648</idno><idno type="wicri:Area/Istex/Checkpoint">000E42</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">000E42</idno><idno type="wicri:doubleKey">0302-9743:2008:Espirito Santo J:characterising:strongly:normalising</idno><idno type="wicri:Area/Main/Merge">004525</idno><idno type="wicri:Area/Main/Curation">004414</idno><idno type="wicri:Area/Main/Exploration">004414</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Characterising Strongly Normalising Intuitionistic Sequent Terms</title><author><name sortKey="Espirito Santo, J" sort="Espirito Santo, J" uniqKey="Espirito Santo J" first="J." last="Espírito Santo">J. Espírito Santo</name><affiliation wicri:level="4"><country xml:lang="fr">Portugal</country><wicri:regionArea>Mathematics Department, University of Minho</wicri:regionArea><placeName><settlement type="city">Braga</settlement><region>Région Nord (Portugal)</region></placeName><orgName type="university">Université du Minho</orgName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Portugal</country></affiliation></author><author><name sortKey="Ghilezan, S" sort="Ghilezan, S" uniqKey="Ghilezan S" first="S." last="Ghilezan">S. Ghilezan</name><affiliation wicri:level="1"><country xml:lang="fr">Serbie</country><wicri:regionArea>Faculty of Engineering, University of Novi Sad</wicri:regionArea><wicri:noRegion>University of Novi Sad</wicri:noRegion></affiliation><affiliation></affiliation></author><author><name sortKey="Iveti, J" sort="Iveti, J" uniqKey="Iveti J" first="J." last="Iveti">J. Iveti</name><affiliation wicri:level="1"><country xml:lang="fr">Serbie</country><wicri:regionArea>Faculty of Engineering, University of Novi Sad</wicri:regionArea><wicri:noRegion>University of Novi Sad</wicri:noRegion></affiliation><affiliation></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><idno type="ISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: This paper gives a characterisation, via intersection types, of the strongly normalising terms of an intuitionistic sequent calculus (where LJ easily embeds). The soundness of the typing system is reduced to that of a well known typing system with intersection types for the ordinary λ-calculus. The completeness of the typing system is obtained from subject expansion at root position. This paper’s sequent term calculus integrates smoothly the λ-terms with generalised application or explicit substitution. Strong normalisability of these terms as sequent terms characterises their typeability in certain “natural” typing systems with intersection types. The latter are in the natural deduction format, like systems previously studied by Matthes and Lengrand et al., except that they do not contain any extra, exceptional rules for typing generalised applications or substitution.</div></front></TEI><affiliations><list><country><li>Portugal</li><li>Serbie</li></country><region><li>Région Nord (Portugal)</li></region><settlement><li>Braga</li></settlement><orgName><li>Université du Minho</li></orgName></list><tree><country name="Portugal"><region name="Région Nord (Portugal)"><name sortKey="Espirito Santo, J" sort="Espirito Santo, J" uniqKey="Espirito Santo J" first="J." last="Espírito Santo">J. Espírito Santo</name></region><name sortKey="Espirito Santo, J" sort="Espirito Santo, J" uniqKey="Espirito Santo J" first="J." last="Espírito Santo">J. Espírito Santo</name></country><country name="Serbie"><noRegion><name sortKey="Ghilezan, S" sort="Ghilezan, S" uniqKey="Ghilezan S" first="S." last="Ghilezan">S. Ghilezan</name></noRegion><name sortKey="Iveti, J" sort="Iveti, J" uniqKey="Iveti J" first="J." last="Iveti">J. Iveti</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 004414 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 004414 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:1CB16E50D217A5407B98673DF326F8AF7574915B
|texte= Characterising Strongly Normalising Intuitionistic Sequent Terms
}}
| This area was generated with Dilib version V0.6.33. |  |